;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
;(require "Iperformance.lisp")
(require "Mperformance.lisp")
(require "DataGenerators.lisp")
(require "Mio.lisp")
(require "Mhelpers.lisp")
;(require "M-avl-string-keys.lisp")
(require "Mstock-retrieval.lisp")

(module Tperformance
  (import Iperformance)
  (import Itree)
  
  ; check-expect tests
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  ;(include-book "testing" :dir :teachpacks)
  
  ; shows the result of the performance query is a string
  ;(check-expect (performance "JOSH" "20111025" "20111025" (read-stocks-file "test.txt")) '("JOSH" 0))
  ;(check-expect (performance-query "JOSH" "20111025" "20111025" (read-stocks-file "test.txt")) "JOSH: 0%")
  
  (include-book "doublecheck" :dir :teachpacks)
  ; random date
  (defrandom random-date ()
    (int->str (random-between 19000101 20990101)))
  
  ; random stock entry from the file, includes the date
  (defrandom random-stocks-file-line ()
    (list (random-date) (random-string) (random-natural) (random-natural)
          (random-natural) (random-natural) (random-natural)))
  
  ; random stock entry from within the sub-trees in the AVL tree
  (defrandom random-stock-entry ()
   (list (random-string) (random-natural) (random-natural)
         (random-natural) (random-natural) (random-natural)))
                                                             
  
  ; random tree - constructs an AVL tree
  ; given a list of stock file lines
  ; using insert-record
  (defun generate-tree (stocks tree)
    (if (consp stocks)
        (let* ((stock (car stocks))
           (date (car stock))
           (ticker (cadr stock))
           (opening-price (caddr stock))
           (highest-price (cadddr stock))
           (lowest-price (car (cddddr stock)))
           (closing-price (car (cdr (cddddr stock))))
           (num-traded (car (cdr (cdr (cddddr stock)))))
           (datalist (list opening-price highest-price lowest-price closing-price num-traded)))
      (if (equal (avl-retrieve tree date) nil)
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (empty-tree) ticker datalist))) ; if the given date doesn't exist, create it in the tree
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (cdr (avl-retrieve tree date)) ticker datalist)))))
        tree))
  
  ; random tree
  (defrandom random-stock-tree ()
    (generate-tree (random-list-of (random-stocks-file-line)) (empty-tree)))

  ; tests that performance-query returns a string
  (defproperty performance-query-returns-string-prp
    (start   :value (random-date)
     end     :value (random-date)
             :where (<= (str->int end) (str->int start))
     tickers :value (random-list-of (random-string))
     tree    :value (random-stock-tree))
    (equal t (stringp (performance-query start end tickers tree))))
  
  )
(link RTperformance (Mtree DataGenerators Mhelpers Mstockretrieval Mperformance Tperformance))
;(invoke RTperformance)